Nuprl Lemma : w-m_wf
0,22
postcript
pdf
the_w
:World,
i
:Id,
t
:
. m(
i
;
t
)
{
m
:Msg(
the_w
.M)| source(mlnk(
m
)) =
i
} List
latex
Definitions
World
,
w
.M
,
m(
i
;
t
)
,
x
:
A
.
B
(
x
)
,
,
t
T
,
Id
Lemmas
Id
wf
,
nat
wf
,
world
wf
origin
the_w:World, i:Id, t:
. m(i;t) 
{m:Msg(the_w.M)| source(mlnk(m)) = i } List the_w:World, i:Id, t:. m(i;t) {m:Msg(the_w.M)| source(mlnk(m)) = i } List x:A. B(x) T